\begin{tabbing}
f{-}rank\=\{i:l\}\+
\\[0ex]($x$; ${\it free}$; ${\it es}$; $e$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if $x$ changed before $e$\+
\\[0ex]then let $r$\= = f{-}rank\=\{i:l\}\+\+
\\[0ex]($x$; ${\it free}$; ${\it es}$; (last change to $x$ before $e$)) in
\-\\[0ex]if eq\_id(es{-}after(${\it es}$; $x$; $e$); ${\it free}$) then inc{-}fst($r$) else inc{-}snd($r$) fi 
\-\\[0ex]else $<$0, 1$>$
\\[0ex]fi 
\\[0ex]
\-\\[0ex]{\em clarification:}
\\[0ex]
\\[0ex]f{-}rank\=\{i:l\}\+
\\[0ex]($x$; ${\it free}$; ${\it es}$; $e$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if changed\=\{i:l\}\+\+
\\[0ex](Id; id{-}deq; ${\it es}$; $x$; $e$)
\-\\[0ex]then let $r$\= = f{-}rank\=\{i:l\}\+\+
\\[0ex]($x$; ${\it free}$; ${\it es}$; last{-}change\{i:l\}(Id; id{-}deq; ${\it es}$; $x$; $e$)) in
\-\\[0ex]if eq\_id(es{-}after(${\it es}$; $x$; $e$); ${\it free}$) then inc{-}fst($r$) else inc{-}snd($r$) fi 
\-\\[0ex]else $<$0, 1$>$
\\[0ex]fi 
\-\\[0ex]\emph{(recursive)}
\end{tabbing}